Issue1946-5.agda:16,16-23
SizeUniv != Set
when checking that the expression Size< i has type Set
